Nuprl Lemma : R-sframe-rule
11,40
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:(Knd List). R-realizes{i:l}(Rsframe(
l
;
tg
;
L
);
es
.sframe-p(
es
;
l
;
tg
;
L
))
latex
Definitions
t
T
,
True
,
P
Q
,
R-Feasible{i:l}(
R
)
,
P
Q
,
R-realizes{i:l}(
R
;
es
.
P
(
es
))
,
x
:
A
.
B
(
x
)
,
R-consistent(
R
;
es
)
,
prop{i:l}
Lemmas
IdLnk
wf
,
Id
wf
,
Knd
wf
,
event
system
wf
,
Rsframe
wf
,
R-consistent
wf
origin
l:IdLnk, tg:Id, L:(Knd List). R-realizes{i:l}(Rsframe(l; tg; L); es.sframe-p(es; l; tg; L)) l:IdLnk, tg:Id, L:(Knd List). R-realizes{i:l}(Rsframe(l; tg; L); es.sframe-p(es; l; tg; L)) 
T
Q
Qx:A. B(x)